es:ES, Q:(EE), X:AbsInterface(Top), p:retrace(es; Q; X). retracer(p)  E(E(X) List) 

latex

Definitions	t  T, x:A. B(x), E, (x  l), b, P  Q, x:AB(x), xL. P(x), P & Q, Top, e  X, Type, , x.A(x), x. t(x), E(X), x:A  B(x), x:A. B(x), f(a), x before y  l, P  Q, type List, s = t, S  T, t.1, let x,y = A in B(x;y), ES, AbsInterface(A), if b then t else f fi , P  Q, retrace(es; Q; X), retracer(p)
Lemmas	retrace wf, es-interface wf, top wf, event system wf, es-E-interface wf, es-E wf, pi1 wf, iff wf, l before wf, list-set-type2, assert wf, es-is-interface wf, l member wf